enrich gen-secdomain
 , 
       gen-systemstate
 , 
       gen-commands , 
       gen-value , 
       gen-name with
comment: tries to add a state that is ignored by the NIF spec. 
         However, it is no good because RMA-2 does not hold for a real system.;
   functions 
      contents : systemstate × name → value;
      comment: Rushby Def. 5;
       
      obs : systemstate × secdomain → systemstate;
      step : systemstate × command → systemstate;
      cdom : command → secdomain;
      ipurged : command → command;
      comment: remove everything except states.;
       
   predicates 
      isState : name;
      comment: addition to original Rushby definition.;
       
      observe : name × secdomain;
      alter : name × secdomain;
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: Rushby Reference Monitor Assumption.;
       
      eqS : systemstate × systemstate;
      comment: additional equality for states.;
       
   
   axioms 
      eqS-def :  ⊦ eqS(sys, sys0) ↔ (∀ nam. isState(nam) → contents(sys, nam) = contents(sys0, nam));
      eqd-def :  ⊦ eqd(sys, d, sys0) ↔ (∀ nam. observe(nam, d) ∧ ¬ isState(nam) → contents(sys, nam) = contents(sys0, nam));
      obs-in-domain :  ⊦ observe(nam, d) ∧ ¬ isState(nam) → contents(obs(sys, d), nam) = contents(sys, nam);
      used for : s, ls;
       
      obs-other-domain :  ⊦ ¬ (observe(nam, d) ∧ ¬ isState(nam)) → contents(obs(sys, d), nam) = null;
      extensionality :  ⊦ sys = sys0 ↔ (∀ nam. contents(sys, nam) = contents(sys0, nam));
      RMA-1 :  ⊦ eqd(sys, d, sys0) → obs(sys, d) = obs(sys0, d);
      comment: can be proved, is no axiom.;
      used for : theorem;
       
      RMA-2
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ eqS(sys, sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ alter(nam, cdom(co))
        → contents(step(sys, co), nam) = contents(step(sys0, co), nam);
      RMA-3 :  ⊦ contents(step(sys, co), nam) ≠ contents(sys, nam) → alter(nam, cdom(co));
      alter-observe-respects-policy :  ⊦ alter(nam, d) ∧ observe(nam, d0) ∧ ¬ isState(nam) → d ⇒ d0;
      eqs-step :  ⊦ eqS(sys, sys0) → eqS(step(sys, co), step(sys0, co));
      ipurged-req :  ⊦ isState(nam) → contents(step(sys, ipurged(co)), nam) = contents(step(sys, co), nam);
      used for : s, ls;
       
      ipurged-not :  ⊦ ¬ isState(nam) → contents(step(sys, ipurged(co)), nam) = contents(sys, nam);
      used for : s, ls;
       
      ipurged-dom :  ⊦ cdom(ipurged(co)) = cdom(co);
      used for : s, ls;
       
      ipurged-id :  ⊦ ipurged(ipurged(co)) = ipurged(co);
      used for : s, ls;
       
end enrich